\begin{tabbing}
val{-}axiom($E$;$V$;$M$;${\it info}$;${\it pred?}$;
\\[0ex]${\it init}$;${\it Trans}$;
\\[0ex]${\it Choose}$;${\it Send}$;${\it val}$;${\it time}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:$E$. \+
\\[0ex]($\uparrow$islocal(kind(${\it info}$;$e$)))
\\[0ex]$\Rightarrow$ ($\exists$\=$x$:$\mathbb{N}$\+
\\[0ex](($\uparrow$isl(\=${\it Choose}$\+
\\[0ex](loc(${\it info}$;$e$)
\\[0ex],act(kind(${\it info}$;$e$))
\\[0ex],$x$
\\[0ex],$\lambda$$x$.state\_when($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$;${\it time}$)($x$,0))))
\-\\[0ex]c$\wedge$ (\=${\it val}$($e$)\+
\\[0ex]=
\\[0ex]outl(\=${\it Choose}$\+
\\[0ex](loc(${\it info}$;$e$)
\\[0ex],act(kind(${\it info}$;$e$))
\\[0ex],$x$
\\[0ex],$\lambda$$x$.state\_when($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$;${\it time}$)($x$,0)))
\-\\[0ex]$\in$ $V$(loc(${\it info}$;$e$),act(kind(${\it info}$;$e$)))))))
\-\-\\[0ex]$\wedge$ \=($\forall$$e$:$E$. \+
\\[0ex]($\uparrow$isrcv(kind(${\it info}$;$e$)))
\\[0ex]$\Rightarrow$ \=($<$lnk(kind(${\it info}$;$e$))\+
\\[0ex], tag(kind(${\it info}$;$e$))
\\[0ex], ${\it val}$($e$)$>$ $\in$ \=${\it Send}$\+
\\[0ex](loc(${\it info}$;sender(${\it info}$;$e$))
\\[0ex],kind(${\it info}$;sender(${\it info}$;$e$))
\\[0ex],${\it val}$(sender(${\it info}$;$e$))
\\[0ex],$\lambda$$x$.\=state\_when(sender(${\it info}$;$e$);${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$;${\it time}$)\+
\\[0ex]($x$
\\[0ex],0)) $\in$ Msg($M$)))
\-\-\-\-\-
\end{tabbing}